(set-logic ALL)
(set-option :model_validate true)
(set-option :model true)
(set-option :rewriter.bv_le_extra true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r7 Real)
(declare-const v6 Bool)
(declare-const bv_15-0 (_ BitVec 15))
(push 1)
(declare-const r9 Real)
(push 1)
(declare-const v7 Bool)
(declare-sort S0 0)
(declare-const r10 Real)
(push 1)
(declare-const v8 Bool)
(pop 1)
(declare-const S0-0 S0)
(declare-const v9 Bool)
(declare-const bv_2-0 (_ BitVec 2))
(declare-const i9 Int)
(declare-const bv_13-0 (_ BitVec 13))
(declare-const v10 Bool)
(declare-const S0-1 S0)
(declare-const v11 Bool)
(pop 1)
(declare-const v12 Bool)
(pop 1)
(push 1)
(declare-const v13 Bool)
(push 1)
(declare-const bv_24-0 (_ BitVec 24))
(push 1)
(declare-const bv_12-0 (_ BitVec 12))
(declare-const r11 Real)
(declare-const v14 Bool)
(declare-sort S0 0)
(declare-const i10 Int)
(declare-const i11 Int)
(pop 1)
(declare-const v15 Bool)
(push 1)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (exists ((q0 (_ BitVec 15))) (not (bvule q0 (bvadd bv_15-0 (bvlshr bv_15-0 bv_15-0))))))
(declare-const r12 Real)
(declare-const v18 Bool)
(declare-const r13 Real)
(pop 1)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(assert (exists ((q1 Bool) (q2 (_ BitVec 24))) (not (distinct q2 (bvxor bv_24-0 bv_24-0 bv_24-0 bv_24-0) q2 bv_24-0 bv_24-0))))
(declare-const i12 Int)
(declare-sort S0 0)
(declare-const r14 Real)
(declare-const bv_11-0 (_ BitVec 11))
(push 1)
(declare-const r15 Real)
(declare-const v22 Bool)
(declare-const r16 Real)
(declare-const r17 Real)
(declare-const v23 Bool)
(declare-sort S1 0)
(declare-const v24 Bool)
(declare-const v25 Bool)
(push 1)
(declare-const v26 Bool)
(declare-const r18 Real)
(declare-const bv_13-0 (_ BitVec 13))
(declare-const v27 Bool)
(declare-const i13 Int)
(declare-const r19 Real)
(declare-const v28 Bool)
(declare-const v29 Bool)
(pop 1)
(declare-const v30 Bool)
(declare-sort S2 0)
(declare-const v31 Bool)
(push 1)
(declare-const v32 Bool)
(declare-const i14 Int)
(declare-const bv_8-5 (_ BitVec 8))
(declare-const S2-0 S2)
(declare-const v33 Bool)
(declare-const v34 Bool)
(declare-const v35 Bool)
(push 1)
(declare-const v36 Bool)
(declare-const v37 Bool)
(push 1)
(declare-const r20 Real)
(assert (forall ((q3 (_ BitVec 9))) (not (distinct q3 ((_ zero_extend 1) ((_ repeat 8) (bvcomp (bvlshr bv_15-0 (bvlshr bv_15-0 bv_15-0)) bv_15-0))) q3))))
(push 1)
(declare-const v38 Bool)
(declare-const S2-1 S2)
(declare-const v39 Bool)
(push 1)
(declare-const r21 Real)
(declare-const v40 Bool)
(declare-const i15 Int)
(declare-const S2-2 S2)
(pop 1)
(declare-const v41 Bool)
(declare-const r22 Real)
(declare-const bv_30-0 (_ BitVec 30))
(declare-const v42 Bool)
(declare-const S1-0 S1)
(declare-const v43 Bool)
(declare-const r23 Real)
(declare-const i16 Int)
(declare-const r24 Real)
(declare-const v44 Bool)
(declare-const v45 Bool)
(declare-const bv_9-3 (_ BitVec 9))
(pop 1)
(declare-const v46 Bool)
(pop 1)
(declare-const v47 Bool)
(declare-const v48 Bool)
(declare-const v49 Bool)
(declare-const v50 Bool)
(declare-const i17 Int)
(declare-const v51 Bool)
(declare-const r25 Real)
(declare-const v52 Bool)
(declare-const bv_20-0 (_ BitVec 20))
(pop 1)
(declare-const r26 Real)
(declare-const v53 Bool)
(declare-const i18 Int)
(declare-const r27 Real)
(pop 1)
(declare-const v54 Bool)
(declare-const S0-0 S0)
(declare-const v55 Bool)
(declare-const r28 Real)
(pop 1)
(declare-sort S1 0)
(declare-const v56 Bool)
(declare-const v57 Bool)
(declare-const bv_15-4 (_ BitVec 15))
(pop 1)
(pop 1)
(declare-sort S0 0)
(declare-const r29 Real)
(declare-const r30 Real)
(assert (forall ((q4 (_ BitVec 15)) (q5 Int) (q6 (_ BitVec 15))) (=> (= q6 bv_15-0 bv_15-0 bv_15-0) (= q5 q5))))
(declare-const i19 Int)
(declare-const v58 Bool)
(push 1)
(declare-const bv_4-0 (_ BitVec 4))
(pop 1)
(declare-const v59 Bool)
(declare-const v60 Bool)
(declare-const v61 Bool)
(declare-const v62 Bool)
(declare-const v63 Bool)
(push 1)
(assert (forall ((q7 (_ BitVec 15))) (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (distinct v3 v0 (distinct v5 v5 v5 v4 v2 v0) v4) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (= bv_15-0 bv_15-0))))
(declare-sort S1 0)
(declare-const i20 Int)
(assert (forall ((q8 (_ BitVec 10)) (q9 (_ BitVec 150)) (q10 (_ BitVec 30))) (= (distinct ((_ repeat 5) (concat (bvshl bv_15-0 bv_15-0) bv_15-0)) ((_ repeat 5) (concat (bvshl bv_15-0 bv_15-0) bv_15-0)) q9 q9) (bvsle q8 q8) (bvsle q10 q10))))
(declare-sort S2 0)
(declare-const v64 Bool)
(pop 1)
(declare-const i21 Int)
(declare-const r31 Real)
(declare-const S0-0 S0)
(declare-const v65 Bool)
(declare-const r32 Real)
(declare-const r33 Real)
(declare-const bv_4-0 (_ BitVec 4))
(declare-const v66 Bool)
(declare-const r34 Real)
(declare-const bv_30-1 (_ BitVec 30))
(declare-const v67 Bool)
(declare-sort S1 0)
(assert (forall ((q11 S1)) (not (distinct q11 q11))))
(declare-const S1-0 S1)
(declare-const bv_13-0 (_ BitVec 13))
(declare-const v68 Bool)
(assert (exists ((q12 (_ BitVec 13)) (q13 Bool) (q14 (_ BitVec 15)) (q15 (_ BitVec 10))) (=> (xor q13 (xor (distinct (distinct v5 v5 v5 v4 v2 v0) v4 v3 v5) v0 v4) (distinct (concat (bvshl bv_15-0 bv_15-0) bv_15-0) (concat (bvshl bv_15-0 bv_15-0) bv_15-0) (concat (bvshl bv_15-0 bv_15-0) bv_15-0) (concat (bvshl bv_15-0 bv_15-0) bv_15-0)) q13) (= q12 bv_13-0 q12 bv_13-0))))
(declare-const v69 Bool)
(declare-const r35 Real)
(declare-const i22 Int)
(declare-const v70 Bool)
(declare-const i23 Int)
(declare-const v71 Bool)
(declare-const i24 Int)
(push 1)
(declare-const S1-1 S1)
(declare-const v72 Bool)
(declare-const v73 Bool)
(declare-const v74 Bool)
(declare-const v75 Bool)
(declare-const v76 Bool)
(declare-sort S2 0)
(declare-const i25 Int)
(declare-const bv_23-0 (_ BitVec 23))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (>= (/ r5 r7) 943)))
(assert (or (> (to_int r3) (abs (- i0 i2 87))) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (>= (/ r5 r7) 943)))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (> (to_int r3) (abs (- i0 i2 87))) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (> (to_int r3) (abs (- i0 i2 87))) (> (to_int r3) (abs (- i0 i2 87))) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (> (to_int r3) (abs (- i0 i2 87))) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (>= (/ r5 r7) 943) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (>= (/ r5 r7) 943) (> (to_int r3) (abs (- i0 i2 87))) (= r32 (to_real i3) (- r0) 7925903988) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (> (to_int r3) (abs (- i0 i2 87))) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (> (to_int r3) (abs (- i0 i2 87))) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (> (to_int r3) (abs (- i0 i2 87))) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ r5 r7) 943)))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (> (to_int r3) (abs (- i0 i2 87))) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (> (to_int r3) (abs (- i0 i2 87))) (>= (/ r5 r7) 943) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ r5 r7) 943)))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (>= (/ r5 r7) 943) (>= (/ r5 r7) 943)))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (>= (/ r5 r7) 943) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (>= (/ r5 r7) 943) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (> (to_int r3) (abs (- i0 i2 87))) (>= (/ r5 r7) 943) (>= (/ r5 r7) 943) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (> (to_int r3) (abs (- i0 i2 87))) (> (to_int r3) (abs (- i0 i2 87))) (> (to_int r3) (abs (- i0 i2 87))) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (= r32 (to_real i3) (- r0) 7925903988) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (> (to_int r3) (abs (- i0 i2 87))) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (>= (/ r5 r7) 943)))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ r5 r7) 943)))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (> (to_int r3) (abs (- i0 i2 87))) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988)))
(assert (or (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10)) (distinct (_ bv801 10) (_ bv801 10) (_ bv801 10))))
(assert (or (>= (/ r5 r7) 943) (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0)) (>= (/ (to_real i3) r2) 858 r30 r34 (/ r5 r7)) (> (to_int r3) (abs (- i0 i2 87)))))
(assert (or (bvslt ((_ repeat 3) bv_15-0) ((_ repeat 3) bv_15-0))))
(assert (or (= r32 (to_real i3) (- r0) 7925903988) (> (to_int r3) (abs (- i0 i2 87))) (>= (/ r5 r7) 943) (= r32 (to_real i3) (- r0) 7925903988) (>= (/ r5 r7) 943)))
(check-sat)
(exit)
